Step of Proof: p-fun-exp_wf 11,40
Inference at * 
Iof proof for Lemma p-fun-exp wf:


  A:Type, f:(A(A + Top)), n:. f^n  A(A + Top) 
latex
 by (Unfold `p-fun-exp` ( 0)) 
CollapseTHEN (Auto) 
latex

C.

Definitionsf^n, primrec(n;b;c), p-id(), x.A(x), f o g  , {i..j}, #$n, x:A. B(x), {x:A| B(x)} , , x:AB(x), left + right, Top, t  T, Type
Lemmasprimrec wf, p-id wf, p-compose wf, int seg wf, nat wf, top wf

origin